R:Realizer.
R-Feasible(R)
 (es:ES. (Possible(R;es) & (i, x:Id. R-discrete(R)(<i, x>)?ff = discrete(i;x)  ))) 

latex

Definitions

Realizer, t  T, x:A. B(x), discrete(i;x), ff, <a, b>, IdDeq, Id, product-deq(A;B;a;b), R-discrete(R), , Type, x:A  B(x), x.A(x), x. t(x), f(x)?z, s = t, x:AB(x), Possible(R;es), P & Q, ES, x:A. B(x), R-Feasible(R), P  Q, P  Q, P  Q, [[R]], d-feasible-discrete(D;discrete), f(x), f(a), b, x  dom(f), a:A fp B(a), Top, left + right, Unit, , b, A, False, PossibleWorld(D;w), t.1, ES(the_w), FairFifo, A c B, World

Lemmas

possible-world wf, fair-fifo wf, w-es wf, not wf, bnot wf, fpf-ap wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, top wf, fpf wf, fpf-trivial-subtype-top, fpf-dom wf, assert wf, R-discrete-property, R-Feasible-Dsys, d-feasible-world, R-Dsys wf, R-Feasible wf, event system wf, R-possible wf, Id wf, fpf-cap wf, bool wf, R-discrete wf, product-deq wf, id-deq wf, bfalse wf, es-isconst wf, es realizer wf